ES{i}  ES{i'} 

latex

Definitions

Type, ES, EqDecider(T), EOrderAxioms(E; pred?; info), x:A. B(x), P  Q, destination(l), SWellFounded(R(x;y)), pred!(e;e'), A, first(e), pred(e), source(l), b, rcv?(e), s = t, link(e), sender(e), e < e', <a,b>, Prop, S  T, kind(e), loc(e), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), x. t(x), x,y. t(x;y), type List, Msg(M), left+right, Unit, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), P  Q, P & Q, x:AB(x), IdLnk, Id, Top, S  T, x:AB(x), AtomFree(T;x), x:A. B(x), f(a), t  T

Lemmas

atom-free-level-subtype, atom-free wf, top wf, Id wf, IdLnk wf, val-axiom wf, unit wf, Msg wf, kindcase wf, Knd wf, loc wf, kind wf, cless wf, sender wf, link wf, rcv? wf, assert wf, lsrc wf, pred wf, first wf, not wf, pred! wf, strongwellfounded wf, ldst wf, EOrderAxioms wf, deq wf, event system wf